Code and Notes (Week 7 Thursday)

-- Week 7B: Algebraic Data Types in Haskell
{-# LANGUAGE EmptyCase #-}
module Main where

-- Product type definition
data Product a b = MkProd a b

-- Haskell's built-in product type uses "tuple" syntax
-- :: (a × b) on the slides
myProd :: (Int, Bool)
myProd = (1, False)

-- Sum type definition
data Sum a b = Inl a | Inr b

myOtherSumL :: Sum Int Bool
myOtherSumL = Inl 1

-- Haskell's built-in sum type is "Either"
-- :: (a + b) on the slides
mySumL :: Either Int Bool
mySumL = Left 1

mySumR :: Either Int Bool
mySumR = Right True

-- Unit type definition
data Unit = Unit

-- Haskell's built-in unit type is () with unit value ()
-- :: 1 on the slides
-- () :: ()
myUnit :: ()
myUnit = ()

-- Empty type definition
-- (NB: The {-# LANGUAGE EmptyCase #-} at the top of the file
-- may be needed to allow us to declare this.)
data Void

-- Haskell's standard library empty type is Data.Void
-- (you can import it)
-- import Data.Void

-- Empty type eliminator: No cases!
-- :: 0 -> a on the slides
absurd :: Void -> a
absurd x = case x of {}

-- Type corresponding to negation in constructive logics
type Not a = a -> Void

-- Functions corresponding to proofs in constructive logics
-- Here, x :: a, and f :: a -> Void, so it's implementable.
two :: a -> Not (Not a)
-- :: a -> ((a -> Void) -> Void)
two x f = f x
-- Note, it's double negation elimination,
--   i.e. Not (Not a) -> a,
-- that doesn't have a constructive proof. To see why,
-- try defining a terminating function of this type!
-- :: ((a -> Void) -> Void) -> a

contra :: (a -> b) -> (Not b -> Not a)
contra f g = g . f

dist_or :: Not (Sum a b) -> ((Not a), (Not b))
dist_or f = (\a -> f (Inl a), \b -> f (Inr b))
-- Note, the backslash \ above is a lambda in Haskell.
-- \_ -> blah corresponds to λ_. blah

-- Some non-terminating functions that are well typed in Haskell
spin :: Int -> Bool
spin = spin

-- These two, if interpreted as proofs, contradict each other:
proof1 :: (Int -> Bool, Bool -> Int) -- Int = Bool ?
proof1 = proof1

proof2 :: Not (Int -> Bool, Bool -> Int) -- Int != Bool ?
proof2 = proof2

-- The list defined in the slides was only for Ints.
-- data IntList = Nil | Cons Int IntList

-- But Haskell supports polymorphic types.
-- Note here the polymorphism of type MyList over
-- type variable a - more info on that in Week 8.
data MyList a = MyNil | MyCons a (MyList a)

-- Here's an example of a recursive type
data BinTree = Leaf | Node BinTree BinTree
-- Its type will use form: rec t . T
-- Using the procedure from the lecture slides
-- we can rewrite it roughly as follows:
-- Leaf | Node BinTree BinTree
-- ~> 1 + 1 × (BinTree × BinTree)
-- ~> rec t. 1 + 1 × (t × t)
-- ~> rec t. 1 + (t × t)

-- Type checking a recursive type

-- Example 1: Leaf
myLeaf :: BinTree
myLeaf = Leaf
-- Leaf ~ roll (Inl ())
--
-- Typing derivation tree:
--
-- (Inl ()) :: 1 + a
-- (Inl ()) ::
--   1 + ((rec t. 1 + (t × t)) × (rec t. 1 + (t × t)))
-- ---------------------------------------------------
--          roll (Inl ()) :: rec t. 1 + (t × t)

-- Example 2: Node Leaf Leaf
myNode :: BinTree
myNode = Node Leaf Leaf
--
-- Typing derivation tree:
--
-- (see Example 1 above for the rest)
-- -----------------------------------
-- roll (Inl ()) :: rec t. 1 + (t × t) <- same hypothesis
-- -----------------------------------    for fst and snd
-- (roll (Inl ()), (Inl ())) ::
--   (rec t. 1 + (t × t)) × (rec t. 1 + (t × t))
-- ---------------------------------------------------
-- Inr (roll (Inl ()), roll (Inl ())) ::
--   1 + ((rec t. 1 + (t × t)) × (rec t. 1 + (t × t)))
-- ---------------------------------------------------
-- roll Inr (roll (Inl ()), roll (Inl ())) ::
--   rec t. 1 + (t × t)

describeT :: (String, Integer) -> String
describeT (s, n) =
  "humans say: " ++ (show s) ++ "\n" ++
  "de Bruijn says: " ++ (show n)

-- For completeness, so the module can be compiled
main :: IO ()
main = putStrLn $ describeT ("x",0)